T:Type, eq:EqDecider(T), es:ES, x:Id, e, e':E.
@loc(e')(x:T)
 e loc e' 
 ((x after lastchange(x;e')) = (x when lastchange(x;e'))  T)
 ((x when e) = (x when e')  T) 

latex

Definitions	{T}, SQType(T), P  Q, P  Q, P & Q, , t  T, P  Q, EqDecider(T), x:A. B(x), ee'.P(e), False, A, @e(xv), A c B, ff, tt, P  Q, if b then t else f fi , lastchange(x;e), @i(x:T)
Lemmas	not-changed, last-change-property, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool sq, bool cases, not wf, bnot wf, changed wf, assert wf, iff wf, bool wf, event system wf, Id wf, es-E wf, es-le wf, es-when wf, es-vartype wf, es-loc-lc, es-loc wf, es-dtype wf, es-lc wf, es-after wf